es{-}dstate{-}after(${\it es}$;$e$)($x$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if es{-}isconst(${\it es}$;es{-}loc(${\it es}$; $e$);$x$) then es{-}after(${\it es}$; $x$; $e$) else $\cdot$ fi